package extensionTools.smvCreator;


import java.util.ArrayList;
import java.util.Collections;
import java.util.Dictionary;
import java.util.Enumeration;
import java.util.Hashtable;
import java.util.Iterator;

import extensionTools.smvCreator.Exceptions.RulesUtilsException;
import extensionTools.smvCreator.Exceptions.SmvDBException;

/**
 * This class implements the Rule interface to create
 * OR\XOR events rule.
 * @author Luba & Dennis
 *
 */
public class EvXor extends Rule 
{

        /**
         * This is the class constructor, all it
         * does is send db to the father c'tor
         * @param db
         */
        public EvXor(DiagramDatabase db) {
                super(db);
        }
        /**
         * This function receives a database and creates the xor
         * rule.
         * @param db the system's Database
         * @return a String in smv which implements the rule
         * @throws RulesUtilsException 
         * @throws SmvDBException 
         */
        @Override
        public String createRule() throws RulesUtilsException, SmvDBException 
        {
        	String rules = "";
        	String procName = "";
        	
        	for (SmvProcess currProc : db.getSmvProcessList()) 
            {
        		procName = currProc.getName();
        		for (ArrayList<Link> currXorList: currProc.getXorLists()) {
        			rules += getXorOrNextCases(db, currXorList, procName, true);
        		}
        		
        		for (ArrayList<Link> currOrList : currProc.getOrLists()) {
        			rules += getXorOrNextCases(db, currOrList, procName, false);
        		}
            }
            return rules;
        }
        
       /**
        * Given a list of links connected to each other by xor/or ,
        * this function builds the next cases for the ev_or or ev_xor events  
        * @param db diagram database
        * @param links a list of links connected by or/xor
        * @param procName the name of the process
        * @param xorFlag true for xor, false for or
        * @return
     * @throws RulesUtilsException 
     * @throws SmvDBException 
        */
        private static String getXorOrNextCases(DiagramDatabase db, ArrayList<Link> links, 
        										String procName, boolean xorFlag) throws RulesUtilsException, SmvDBException
        {
        	ArrayList<String> objList = new ArrayList<String>();
        	Dictionary<String, String> dict = new Hashtable<String, String>();
        	Dictionary<String, ArrayList<String>> dictOrdinaryObj = new Hashtable<String, ArrayList<String>>();
        	//The main string variable which will include the or/xor rules
        	String rules = "";
        	String xor_or = xorFlag ? "xor" : "or";
        	
        	Dictionary<String, String> objInitState = new Hashtable<String, String>();
        	//create objList - the list of objects connected by the xor/or
        	for (Link currLink : links) {
				long currObjId = currLink.getDstId();
				SmvObject currObj = RulesUtils.getObjectbyId(currObjId, db);
				// If currObjId is of a state rather than an object
				if (currObj == null) {
					int stateId = db.findStateById(currObjId);
					State state = RulesUtils.getStatebyId(stateId, db);
					currObj = RulesUtils.getObjectbyId(state.getObjectId(), db);
				}
				
				//find if object has initial state
				State  initState = currObj.getInitialState();
				if (null != initState)
				{
					objInitState.put(currObj.getName(), "_" + initState.getName());
				}
				//if the link points to a state, this state should be the initial
				if (currLink.getDstId() != currObj.getId())
				{ 
					State dstState = currObj.idBelongsToObj(currLink.getDstId());
					if(null != dstState) 
					{
						objInitState.put(currObj.getName(), "_"+dstState.getName());
					}
					else
					{
		        		throw new SmvDBException("EvXor: A link:"+ currLink + " " +
		        				"that belongs to Object"+ currObj.getName()
		    				+"and her source is a process do not point to and Object " +
		    						"or to one of its " +"states");
					}
				}
				objList.add(currObj.getName());

			}
			if (objList.size() > 1) {
					dict = RulesUtils.getXorDict(procName, objList, xorFlag);
					dictOrdinaryObj = RulesUtils.getLikeXorDict(procName, objList,xorFlag);;
			}
			else {
				throw new SmvDBException("EvXor: No objects found for" + xor_or + "link");
			}
			Enumeration<String> keys = dict.keys();
			while (keys.hasMoreElements()) {
	        	ArrayList<String> temp = new ArrayList<String>();
				String currEventName = keys.nextElement();
				String procFullName = RulesUtils.getProcFullName(currEventName, procName, xorFlag);
				String ev_create = "ev_create_"+procFullName;
				ArrayList<String> instance = dictOrdinaryObj.get(currEventName);
				Iterator<String> iterObjects = objList.iterator();
				Iterator<String> iterInstance = instance.iterator();
				String finalCheckEvCreate = "";
				//iterating over the object and objects instances in this ev_xor/ev_or name
				ArrayList<String> objectsWithInstances = new ArrayList<String>();

				while (iterObjects.hasNext() && iterInstance.hasNext())
				{
					String obj = iterObjects.next();
					String ins = iterInstance.next();
					String initialState = objInitState.get(obj);
					if (initialState == null)
					{
						initialState = "";
					}
					finalCheckEvCreate = SmvOp.and(finalCheckEvCreate, ev_create+"_"+obj+initialState+" = " + ins);
					//Create a list of all the objects with their instances relevant for the or/xor case
					objectsWithInstances.add(obj + "_" + ins);
				}

				for (int index = objectsWithInstances.size(); index > 0 ; index--){
					//Create a dictionary whose keys are strings representing objects with the chosen 
					//states for them (exist/notExist) connected by "and" conditions, and the values are strings
					//representing the objects chose to be "notExist", which can be chosen to be created by
					//the xor/or condition
					Dictionary<String, String> combinationBySize = RulesUtils.getCombinationsByIndex(objectsWithInstances, index, xorFlag);
					Enumeration<String> combinations_enum = combinationBySize.keys();
					ArrayList<String> combinations = Collections.list(combinations_enum);
					for (String s : combinations) {
						
						String ruleLine = SmvOp.createCaseLine(SmvOp.and(SmvOp.and("sysState = event2", 
							"ev_terminate_" + procFullName + " = 0",
							finalCheckEvCreate), s),
							"{" + combinationBySize.get(s) + "}");
						temp.add(ruleLine);
					}
				}
				objectsWithInstances.removeAll(objectsWithInstances);
				//temp[0] = SmvOp.createCaseLine(SmvOp.and(SmvOp.and("sysState = event2", 
				//		procFullName + " = notActive"), "ev_terminate_" + procFullName + " = 0",
				//		finalCheckEvCreate), 
				//		"{" + dict.get(currEventName) + "}");
				//turn off ev_xor
				temp.add(SmvOp.createCaseLine(SmvOp.and("sysState = event2", currEventName + " != false"), "false"));
				temp.add(SmvOp.createCaseLine("TRUE", currEventName));
				rules += "\n" + SmvOp.next(currEventName, SmvOp.createCase(RulesUtils.arrayListToArray(temp)));
				temp.removeAll(temp);

			}
			return rules;
        }
}
